;;; -*- Mode: Lisp; Syntax: Common-Lisp; Package: snark-infix-reader -*-
;;; File: infix-reader.lisp
;;; The contents of this file are subject to the Mozilla Public License
;;; Version 1.1 (the "License"); you may not use this file except in
;;; compliance with the License. You may obtain a copy of the License at
;;; http://www.mozilla.org/MPL/
;;;
;;; Software distributed under the License is distributed on an "AS IS"
;;; basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See the
;;; License for the specific language governing rights and limitations
;;; under the License.
;;;
;;; The Original Code is SNARK.
;;; The Initial Developer of the Original Code is SRI International.
;;; Portions created by the Initial Developer are Copyright (C) 1981-2006.
;;; All Rights Reserved.
;;;
;;; Contributor(s): Mark E. Stickel <stickel@ai.sri.com>.

(in-package :snark-infix-reader)

;;; no operator should be declared to be both infix and postfix
;;; to ease parsing as in ISO Prolog standard

;;; <identifier> = <ordinary-char>+ (but first character cannot be a digit)
;;; <number> = [<sign>] <digit>+ <decimal-point> <digit>+ for floats 
;;;            [<sign>] <digit>+ <forward-slash> <digit>+ for ratios
;;;            [<sign>] <digit>+                          for integers

(definline ordinary-char-p (char)
  (or (alpha-char-p char)
      (digit-char-p char)
      (eql #\_ char)
      (eql #\? char)))					;for SNARK variables

(definline separator-char-p (char)
  (or (eql #\, char)					;comma is not an operator
      (eql #\( char)
      (eql #\) char)
      (eql #\[ char)
      (eql #\] char)
      (eql #\. char)))					;dot is not an operator

(definline whitespace-char-p (char)
  (or (eql #\space char)
      (eql #\tab char)
      (eql #\newline char)
      (eql #\return char)
      (eql #\linefeed char)
      (eql #\page char)))

(definline quotation-char-p (char)
  (or (eql #\" char)
      (eql #\' char)))

(definline comment-char-p (char)
  (eql #\% char))

(defun tokenize1 (string &key (start 0) (end (length string)) (case :preserve) (upper-case-var-prefix #\?) rationalize)
  (let ((pos start))
    (labels
      ((tokenize-identifier ()
         (let ((start pos))
           (incf pos)
           (loop
             (cond
              ((eql end pos)
               (return))
              ((ordinary-char-p (char string pos))
               (incf pos))
              (t
               (return))))
           (let ((token (subseq string start pos)))
             ;; so that variables can be distingished from nonvariables even after upcasing
             ;; if upper-case-var-prefix is a character such as #\_ or #\?
             ;; tokenize adds it to the front of each identifier that starts with
             ;; either an upper-case character
             ;; or one or more of it followed by an alphabetic character
             ;; (read-infix-term "r(x,?,?1,X,?X,??X)") -> (R X ? ?1 ?X ??X ???X)
             (when (and upper-case-var-prefix
                        (let ((c (char token 0)))
                          (or (upper-case-p c)
                              (and (eql upper-case-var-prefix c) 
                                   (dotimes (i (- (length token) 1) nil)
                                     (setf c (char token (+ i 1)))
                                     (cond
                                      ((alpha-char-p c)
                                       (return t))
                                      ((not (eql upper-case-var-prefix c))
                                       (return nil))))))))
               (setf token (concatenate 'string (list upper-case-var-prefix) token)))
             (operator-lookup
              (ecase case
                (:upcase (nstring-upcase token))
                (:downcase (nstring-downcase token))
                (:preserve token))))))
       (tokenize-special ()
         (let ((start pos))
           (incf pos)
           (loop
             (cond
              ((eql end pos)
               (return))
              ((let ((ch (char string pos)))
                 (and (not (ordinary-char-p ch))
                      (not (separator-char-p ch))
                      (not (whitespace-char-p ch))
                      (not (quotation-char-p ch))
                      (not (comment-char-p ch))))
               (incf pos))
              (t
               (return))))
           (operator-lookup (subseq string start pos))))
       (tokenize-number ()
         (let ((num 0) (d 10) n ch cv float ratio)
           (loop
             (cond
              ((eql end pos)
               (return))
              ((setf cv (digit-char-p (setf ch (char string pos))))
               (cond
                (float
                 (setf n (+ (* 10 n) cv) d (* 10 d)))
                (ratio
                 (setf n (+ (* 10 n) cv)))
                (t
                 (setf num (+ (* 10 num) cv))))
               (incf pos))
              ((and (not (or float ratio))
                    (or (eql #\. ch) (eql #\/ ch))	;. for floats, / for ratios
                    (let ((pos (+ pos 1)))
                      (and (not (eql end pos))
                           (setf n (digit-char-p (char string pos))))))
               (if (eql #\. ch) (setf float t) (setf ratio t))
               (incf pos 2))
              (t
               (return))))
           (cond
            (float
             (+ num (/ (if rationalize n (float n)) d)))
            (ratio
             (/ num n))
            (t
             num))))
       (tokenize-string (quotechar)
         (let* ((start (+ pos 1))
                (stop (position quotechar string :start start :end end)))
           (unless stop
             (error "Syntax error: no closing string quotation character"))
           (setf pos (+ stop 1))
           (ecase quotechar
             (#\"
              (subseq string start stop))
             (#\'
              ;; any characters can be put into a symbol by using '...' quotation
              ;; this suppresses default case mangling, var-prefixing, and operator lookup
              ;; however, (tokenize1 "?") = (tokenize1 "'?'") etc.
              ;; so it cannot make a variable denoting token into a nonvariable symbol
              (intern (subseq string start stop))))))
       (operator-lookup (name)
         ;; return an operator interpretation if there is one
         ;; we can lookup the correct interpretation later
         (or (infix-operator-lookup name)
             (prefix-operator-lookup name)
             (postfix-operator-lookup name)
             (intern name))))
      (let (ch)
        ;; skip whitespace and comments
        (let ((in-comment nil))
          (loop
            (cond
             ((<= end pos)
              (return-from tokenize1 (values nil nil)))
             (in-comment
              ;; comment from comment-char through end of line
              (when (or (eql #\newline (setf ch (char string pos)))
                        (eql #\return ch)
                        (eql #\linefeed ch))
                (setf in-comment nil))
              (incf pos))
             ((whitespace-char-p (setf ch (char string pos)))
              (incf pos))
             ((comment-char-p ch)
              (setf in-comment t)
              (incf pos))
             (t
              (return)))))
        (values
         (cond
          ((separator-char-p ch)
           (incf pos)
           ch)
          ((digit-char-p ch)
           (tokenize-number))
          ((ordinary-char-p ch)
           (tokenize-identifier))
          ((quotation-char-p ch)
           (tokenize-string ch))
          ((eql #\+ ch)
           (let ((pos+1 (+ pos 1)))
             (if (and (> end pos+1) (digit-char-p (char string pos+1)))
                 (progn (setf pos pos+1) (tokenize-number))
                 (tokenize-special))))
          ((eql #\- ch)
           (let ((pos+1 (+ pos 1)))
             (if (and (> end pos+1) (digit-char-p (char string pos+1)))
                 (progn (setf pos pos+1) (- (tokenize-number)))
                 (tokenize-special))))
          (t
           (tokenize-special)))
         pos)))))

(defun tokenize (string &key (start 0) (end (length string)) (case :preserve) (upper-case-var-prefix #\?) rationalize)
  (let ((pos start)
        (tokens nil) tokens-last token)
    (loop
      (multiple-value-setq (token pos) (tokenize1 string :start pos :end end :case case :upper-case-var-prefix upper-case-var-prefix :rationalize rationalize))
      (if (null pos)
          (return)
          (collect token tokens)))
    tokens))

;;; converts "p(a,b,c)" to (p a b c)
;;; converts "[a,b,c]" to ($$list a b c)
;;; converts "[a,b|c]" to ($$list* a b c)

(defun tokens-to-lisp (tokens)
  (let ((stack '(#\.))					;stack contains terms, operators, #\(s, #\.
        token1)
    (labels
      ((tokens-to-lisp1 ()
         (cond
          ((or (eql #\( token1) (numberp token1) (stringp token1))
           (cond
            ((starting-term)
             (push token1 stack))
            (t
             (error "Syntax error."))))
          ((symbolp token1)
           (cond
            ((or (eq '-- token1) (eq '++ token1))	;cheat for TPTP without operator declarations and postprocessing
             (let ((neg (eq '-- token1)))
               (cond
                ((starting-term)
                 (setf token1 (pop tokens))
                 (tokens-to-lisp1)
                 (when neg
                   (push (list 'not (pop stack)) stack)))
                (t
                 (error "Syntax error.")))))
            ((starting-term)
             (push (if (eql #\( (first tokens))
                       (progn
                         (setf tokens (rest tokens))
                         (cons token1 (tokens-to-lisp2 '(#\)))))
                       token1)
                   stack))
            (t
             (error "Syntax error."))))
          ((eql #\[ token1)
           (cond
            ((starting-term)
             (push (tokens-to-lisp2 '(#\])) stack))
            (t
             (error "Syntax error."))))
          ((eql #\) token1)
           (cond
            ((not (starting-term))
             (reduce-all #\())
            (t
             (error "Syntax error."))))
          ((operator-p token1)
           ;; is it the right kind of operator?
           ;; if not, just use it as a symbol
           (setf token1 (operator-input-string token1))
           (cond
            ((starting-term)
             (cond
              ((operator-p (setf token1 (or (prefix-operator-lookup token1) (intern token1))))
               (push token1 stack))
              (t
               (tokens-to-lisp1))))
            (t
             (cond
              ((operator-p (setf token1 (or (infix-operator-lookup token1) (postfix-operator-lookup token1) (intern token1))))
               (reduce-before token1)
               (push token1 stack))
              (t
               (tokens-to-lisp1))))))
          (t
           (error "Syntax error."))))
       (tokens-to-lisp2 (brackets)
         ;; convert lists and argument lists
         (let ((list* nil)
               (args nil)
               (l nil))
           (loop
             (cond
              ((or (null tokens) (eql #\. (setf token1 (pop tokens))))
               (error "Syntax error."))
              ((eql #\( token1)
               (push #\) brackets)
               (push token1 l))
              ((eql #\[ token1)
               (push #\] brackets)
               (push token1 l))
              ((or (eql #\) token1) (eql #\] token1))
               (cond
                ((not (eql token1 (pop brackets)))
                 (error "Syntax error."))
                ((null brackets)
                 (cond
                  ((null l)
                   (when args
                     (error "Syntax error.")))
                  (t
                   (push (tokens-to-lisp (nreverse l)) args)))
                 (setf args (nreverse args))
                 (return (if (eql #\] token1) (cons (if list* '$$list* '$$list) args) args)))
                (t
                 (push token1 l))))
              ((and (null (rest brackets))
                    (eql #\] (first brackets))
                    ;; treat vertical bar as a separator only in lists
                    (cond
                     ((symbolp token1)
                      (when (string= "|" (symbol-name token1))
                        (setf token1 #\|))
                      nil)
                     ((operator-p token1)
                      (when (string= "|" (operator-input-string token1))
                        (setf token1 #\|))
                      nil)
                     (t
                      nil)))
               )
              ((and (null (rest brackets)) (or (eql #\, token1) (and (eq #\| token1) (eql #\] (first brackets)))))
               (cond
                ((null l)
                 (error "Syntax error."))
                (list*
                 (error "Syntax error."))
                (t
                 (push (tokens-to-lisp (nreverse l)) args)))
               (setf l nil)
               (setf list* (eq #\| token1)))
              (t
               (push token1 l))))))
       (reduce-once ()
         (let ((x (pop stack)) (y (pop stack)) z)
           (cond
            ((infix-operator-p y)
             (if (and (operand-p (setf z (pop stack))) (operand-p x))
                 (push (list (operator-output-symbol y) z x) stack)
                 (error "Syntax error.")))
            ((prefix-operator-p y)
             (if (operand-p x)
                 (push (list (operator-output-symbol y) x) stack)
                 (error "Syntax error.")))
            ((postfix-operator-p x)
             (if (operand-p y)
                 (push (list (operator-output-symbol x) y) stack)
                 (error "Syntax error.")))
            (t
             (error "Syntax error.")))))
       (reduce-before (op)
         (loop
           (if (cond
                ((operator-p (first stack))
                 (reduce-before? (first stack) op))
                ((operator-p (second stack))
                 (reduce-before? (second stack) op))
                (t
                 nil))
               (reduce-once)
               (return))))
       (reduce-all (start)
         (loop
           (cond
            ((and (operand-p (first stack)) (eql start (second stack)))
             (setf stack (cons (first stack) (rest (rest stack))))
             (return))
            (t
             (reduce-once)))))
       (starting-term ()
         (let ((top (first stack)))
           (not (or (operand-p top) (postfix-operator-p top)))))
       (operand-p (x)
         (not (or (eql #\( x) (eql #\. x) (operator-p x)))))
      (loop
        (cond
         ((or (null tokens) (eql #\. (setf token1 (pop tokens))))
          (reduce-all #\.)
          (return))
         (t
          (tokens-to-lisp1))))
      (values (if (null (rest stack)) (first stack) stack) tokens))))

(defun read-infix-term (x &key (start 0) (end nil) (case :preserve) (upper-case-var-prefix #\?) rationalize)
  ;; read one term from x and return it and list of leftover tokens
  ;; if x is a string, tokenize it
  ;; if x is a list, assume it is a tokenized string (with correct case and upper-case-var-prefix)
  (when (stringp x)
    (setf x (tokenize x :start start :end (or end (length x)) :case case :upper-case-var-prefix upper-case-var-prefix :rationalize rationalize)))
  (cl:assert (consp x))
  (tokens-to-lisp x))

(defun read-infix-terms (x &key (start 0) (end nil) (case :preserve) (upper-case-var-prefix #\?) rationalize)
  (when (string x)
    (setf x (tokenize x :start start :end (or end (length x)) :case case :upper-case-var-prefix upper-case-var-prefix :rationalize rationalize)))
  (let ((terms nil) terms-last term)
    (loop
      (cond
       ((null x)
        (return terms))
       (t
        (multiple-value-setq (term x) (tokens-to-lisp x))
        (collect term terms))))))

;;; infix-reader.lisp EOF
